\begin{tabbing}
$\forall$$i$:Id, $p$:finite{-}prob{-}space, ${\it ds}$:fpf(Id; $x$.Type), $P$:(decl{-}state(${\it ds}$)$\rightarrow\mathbb{B}$).
\\[0ex]normal{-}ds\=\{i:l\}\+
\\[0ex](${\it ds}$)
\-\\[0ex]$\Rightarrow$ es{-}real\=\{i:l\}\+
\\[0ex](${\it es}$.@$i$ Precondition for mkid\{a:ut2\}(Outcome($p$)) $P$ discrete state(${\it ds}$))
\-
\end{tabbing}